Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,n__from(n__s(X)))
2:    sel(0,cons(X,XS))  → X
3:    sel(s(N),cons(X,XS))  → sel(N,activate(XS))
4:    minus(X,0)  → 0
5:    minus(s(X),s(Y))  → minus(X,Y)
6:    quot(0,s(Y))  → 0
7:    quot(s(X),s(Y))  → s(quot(minus(X,Y),s(Y)))
8:    zWquot(XS,nil)  → nil
9:    zWquot(nil,XS)  → nil
10:    zWquot(cons(X,XS),cons(Y,YS))  → cons(quot(X,Y),n__zWquot(activate(XS),activate(YS)))
11:    from(X)  → n__from(X)
12:    s(X)  → n__s(X)
13:    zWquot(X1,X2)  → n__zWquot(X1,X2)
14:    activate(n__from(X))  → from(activate(X))
15:    activate(n__s(X))  → s(activate(X))
16:    activate(n__zWquot(X1,X2))  → zWquot(activate(X1),activate(X2))
17:    activate(X)  → X
There are 16 dependency pairs:
18:    SEL(s(N),cons(X,XS))  → SEL(N,activate(XS))
19:    SEL(s(N),cons(X,XS))  → ACTIVATE(XS)
20:    MINUS(s(X),s(Y))  → MINUS(X,Y)
21:    QUOT(s(X),s(Y))  → S(quot(minus(X,Y),s(Y)))
22:    QUOT(s(X),s(Y))  → QUOT(minus(X,Y),s(Y))
23:    QUOT(s(X),s(Y))  → MINUS(X,Y)
24:    ZWQUOT(cons(X,XS),cons(Y,YS))  → QUOT(X,Y)
25:    ZWQUOT(cons(X,XS),cons(Y,YS))  → ACTIVATE(XS)
26:    ZWQUOT(cons(X,XS),cons(Y,YS))  → ACTIVATE(YS)
27:    ACTIVATE(n__from(X))  → FROM(activate(X))
28:    ACTIVATE(n__from(X))  → ACTIVATE(X)
29:    ACTIVATE(n__s(X))  → S(activate(X))
30:    ACTIVATE(n__s(X))  → ACTIVATE(X)
31:    ACTIVATE(n__zWquot(X1,X2))  → ZWQUOT(activate(X1),activate(X2))
32:    ACTIVATE(n__zWquot(X1,X2))  → ACTIVATE(X1)
33:    ACTIVATE(n__zWquot(X1,X2))  → ACTIVATE(X2)
The approximated dependency graph contains 4 SCCs: {20}, {22}, {25,26,28,30-33} and {18}.
Tyrolean Termination Tool  (2.90 seconds)   ---  May 3, 2006